%%This is a very basic article template.
%%There is just one section and two subsections.
\documentclass{llncs}
\usepackage{graphicx}
\usepackage{multirow}
\usepackage{amsmath}
%\usepackage{times}
\usepackage[scriptsize]{subfigure}
\usepackage{listings}
\usepackage[outerbars]{changebar}

% uncomment to hide changebars
\nochangebars
\tolerance5000

\lstset{ % Configure listings
	captionpos=b,
	breaklines=true,
	xleftmargin=8pt,
	basicstyle=\sffamily\fontsize{8pt}{9pt}\selectfont,
        keywordstyle=\sffamily\fontsize{8pt}{9pt}\selectfont\bfseries,
	numberstyle=\tiny,
	flexiblecolumns=true,
	nolol=true,
	tabsize=2,
        numberbychapter=false,
	numbersep=5pt,
}

\lstdefinelanguage{ATL}{
        keywords={rule,module,from,to,create,uses,lazy,unique,helper},
        morekeywords={context,def,let,in,if,then,else,endif,inv},
        morekeywords={and,or},
        morekeywords={do},
        emph={Boolean,Integer,String,Sequence},
        sensitive=true,
        morecomment=[l]{--},
        morestring=[b]',
        showstringspaces=false,
}

\setlength{\intextsep}{7pt plus 1.0pt minus 3.0pt}
\setlength{\textfloatsep}{7pt plus 1.0pt minus 3.0pt}
\setlength{\floatsep}{7pt plus 1.0pt minus 3.0pt}

% for subfloats as environment
\newbox\subfigbox
\makeatletter
\newenvironment{subfloat}
{\def\caption##1{\gdef\subcapsave{\relax##1}}%
\let\subcapsave\@empty
\setbox\subfigbox\hbox
\bgroup}
{\egroup
\subfigure[\subcapsave]{\box\subfigbox}}
\makeatother


\begin{document}
\title{Automated Verification of Model Transformations in the Automotive
Industry\thanks{This work was partially funded by the Nouvelles \'Equipes
Program of the Pays de la Loire Region (France), and by NSERC (Canada), as part
of the NECSIS Automotive Partnership with General Motors, IBM Canada and Malina
Software Corp.}}

\titlerunning{Automated Verification of Model Transformations in the Automotive
Industry}
%\subtitle{Do you have a subtitle?\\ If so, write it here}
\author{Gehan M. K. Selim\inst{1} \and Fabian B\"uttner\inst{2} \and James
R. Cordy\inst{1} \and Juergen Dingel\inst{1} \and Shige Wang\inst{3}
% \thanks is optional - remove next line if not needed
}                     % Do not remove
 \institute{School of Computing, Queen{'}s University, Kingston,
 Ontario, Canada \and AtlanMod, \'Ecole des Mines de Nantes - INRIA, LINA, Nantes, France \and Electrical and Controls Integration Lab, General Motors
 Research and Development, Warren, Michigan, USA}
\date{Received: date / Revised version: date}
\maketitle
\setcounter{footnote}{0}
\begin{abstract}
% Many companies have adopted Model Driven Development (MDD) for
% developing their software systems. Several studies have reported
% on such industrial experiences by discussing the positive effects that MDD has
% had and the issues that still need to be addressed. However, only a few studies
% have specifically discussed using automated verification to check the
% correctness of industrial model transformations. In a previous study we
% demonstrated in detail how transformations can be used to migrate GM legacy
% models to the new AUTOSAR standard in the automotive industry. In this study, we
% investigate using automated verification for such industrial applications of
% transformations. We report on applying an automated verification approach to
% the GM-to-AUTOSAR transformation that is based on checking the satisfiability
% of a relational transformation representation, or a \emph{transformation model},
% with respect to well-formedness OCL constraints. An implementation of this
% approach is available as a research prototype for the ATL transformation
% language. We present the verification results of this transformation and discuss
% the practicality of using such tools on industrial-size problems.
Many companies have adopted MDD for developing their software systems. Several
studies have reported on such industrial experiences by discussing the effects
of MDD and the issues that still need to be addressed. However, only a few
studies have discussed using automated verification of industrial model
transformations. We previously demonstrated how transformations can be used to
migrate GM legacy models to AUTOSAR models. In this study, we investigate using
automated verification for such industrial transformations. We report on
applying an automated verification approach to the GM-to-AUTOSAR transformation
that is based on checking the satisfiability of a relational transformation
representation, or a transformation model, with respect to well-formedness OCL
constraints. An implementation of this approach is available as a prototype for
the ATL language. We present the verification results of this transformation and
discuss the practicality of using such tools on industrial size problems.
\keywords{Model Transformation, Automated Verification,
Automotive Industry}
\end{abstract}
\vspace{-0.1cm}
 % NOT required for Proceedings
%\section{Title}
%old : Model Driven Development, Model Transformation, Automated Verification,
% ATL, Automotive Industry, Invariants, Contracts.
\section{Introduction}
\label{sec:intro}
\input{introduction}
%Your text comes here. Separate text sections with
\section{Background: Model Transformation in the Automotive Industry}
\label{sec:MT_AutomotiveIndustry}
\input{MT_AutomotiveIndustry}
	\subsection{Overview of the Model Transformation Problem}
	\label{subsec:Overview_MT_Problem}
	\input{Overview_MT_Problem}
%
	\subsection{The GM Metamodel}
	\label{subsec:TheGMmm}
	\input{TheGMmm}
%
	\subsection{The AUTOSAR Metamodel}
	\label{TheAUTOSARmm}
	\input{TheAUTOSARmm}
\section{Verification Methodology}
\label{sec:FormalVer_ConstSolvers}
\input{FormalVer_ConstSolvers}
%
%
\section{Case Study: Evaluating Transformations in
the Automotive Industry Using Automated Verification}
\label{sec:caseStudy}
\input{caseStudy}
	\subsection{Reimplementation of the GM-to-AUTOSAR Model Transformation}
	\label{subsec:reimplementationMT}
	\input{reimplementationMT}
%
	\subsection{Formulation of OCL Pre- and Postconditions}
	\label{subsec:FormulationOCLConsts}
	\input{FormulationOCLConsts}
\section{Results}
\label{sec:results}
\input{results}
	\subsection{Verifying the Formulated OCL Constraints}
	\label{subsec:VerifFormOCLConsts}
	\input{VerifFormOCLConsts}
	%
	\subsection{Performance of the Verification Approach}
	\label{subsec:Scalability}
	\input{Scalability}
	%
\section{Discussion}
\label{sec:discussion}
\input{discussion}
  	\subsection{Strengths of the Verification Approach}
  	\label{subsec:strengthPropApp}
 	\input{strengthPropApp}
 	%%
  	\subsection{Limitations of the Verification Approach}
  	\label{subsec:threatsToValidity}
  	\input{threatsToValidity}
%
\section{Related Work}
\label{sec:RelatedWork}
\input{RelatedWork}
%
\section{Conclusion and Future Work}
\label{sec:concFW}
\input{concFW}
% \begin{acknowledgements}
% This work is supported in part by NSERC, as part of the NECSIS Automotive
% Partnership with General Motors, IBM Canada and Malina Software Corp.
% \end{acknowledgements}
\newpage
 \bibliographystyle{abbrv}
 \bibliography{MODELS_bib}
%
\end{document}
